$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $a$:ecl(${\it ds}$; ${\it da}$), $n$:$\mathbb{N}$. eclact($a$; $n$) $\in$ ecl(${\it ds}$; ${\it da}$)